\begin{tabbing}
$\forall$\=${\it es}$:ES, $l$:IdLnk, ${\it tgs}$:Id List, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $f_{1}$,\+
\\[0ex]$f_{2}$:(\{$e$:E$\mid$ loc($e$) $=$ source($l$) $\in$ Id \}$\rightarrow$((${\it tg}$:Id$\times$${\it da}$(rcv($l$,${\it tg}$))?Void) List)), ${\it ds}_{1}$,
\\[0ex]${\it ds}_{2}$:$x$:Id fp$\rightarrow$ Type.
\-\\[0ex]${\it ds}_{2}$ $\subseteq$ ${\it ds}_{1}$
\\[0ex]$\Rightarrow$ ($\forall$$e$:\{$e$:E$\mid$ loc($e$) $=$ source($l$) $\in$ Id \}. $f_{1}$($e$) $=$ $f_{2}$($e$))
\\[0ex]$\Rightarrow$ with decls ${\it ds}_{1}$ ${\it da}$sends on $l$ from $e$ include $f_{1}$($e$) and only these for tags in ${\it tgs}$
\\[0ex]$\Rightarrow$ with decls ${\it ds}_{2}$ ${\it da}$sends on $l$ from $e$ include $f_{2}$($e$) and only these for tags in ${\it tgs}$
\end{tabbing}